k:Knd, l:IdLnk, tg:Id. (isrcv(k))  (lnk(k) = l)  (tag(k) = tg)  (rcv(l,tg) = k) 

latex

Definitions	x:A. B(x), P  Q, t  T, , rcv(l,tg), Knd, lnk(k), tag(k), outl(x), t.1, t.2, b, isrcv(k), isl(x), ff, if b then t else f fi , False
Lemmas	Id wf, tagof wf, IdLnk wf, lnk wf, assert wf, isrcv wf, Knd wf